A:Type, eq:EqDecider(A), L:(A List), x:A. (deq-member(eq; x; L))  (x  L) 

latex

Definitions	x:A. B(x), b, deq-member(eq; x; L), reduce(f; k; as), ff, Y, if b then t else f fi , t  T, P  Q, P  Q, P  Q, P  Q, P  Q, prop{i:l}, guard(T), False, decidable(P)
Lemmas	deq wf, decidable false, nil member, iff functionality wrt iff, assert wf, bor wf, eqof wf, deq-member wf, l member wf, assert of bor, cons member, or functionality wrt iff, deq property